p, q:IdLnk List, i, j, k:Id.
lconnects(p;i;j)  lconnects(q;j;k)  (r:IdLnk List. lconnects(r;i;k)) 

latex

Definitions	t  T, x:A. B(x), True, T, x:A. B(x), P  Q, Prop, hd(l), Y, ||as||, P & Q, lconnects(p;i;j), P  Q, if b t else f fi, false, null(as), b, P  Q, A, False, lpath(p), true, i<j, b, ij, nth_tl(n;as), l[i], last(L), AB, i  j < k, {i..j}, P  Q, Dec(P)
Lemmas	IdLnk wf, Id wf, true wf, squash wf, lconnects wf, non neg length, length wf1, ldst wf, lpath cons, not wf, false wf, last cons, int seg wf, lnk-inv wf, decidable equal IdLnk, length cons